Skip to content

Implement conversion to SMT for more bit wise expressions #6722

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 3 commits into from
Mar 11, 2022
Merged

Implement conversion to SMT for more bit wise expressions #6722

merged 3 commits into from
Mar 11, 2022

Conversation

thomasspriggs
Copy link
Contributor

This PR adds implements of conversion to SMT for more bit wise expressions.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@thomasspriggs
Implement extract_bits conversion
afda322 
This only works so long as the bits to extract are constant values. This
is the same limitation as is present in the old back end. The reason for
this is limitation is due to the way the `extract` operation is defined
in the smtlib version of bitvector theory. It may be possible to work
around this limitation but the work around is unlikely to be trivial.
@thomasspriggs
Refactor conversion of shift operators
283d3bd 
In preparation for adding conversion of shifts with operands of
mismatched sizes.
@thomasspriggs
Add support for converting mismatched shift operands to smt
5ecedf8 
In order to bring this conversion closer to parity with the old SMT
backend.

Shift operations of this kind have been seen during testing of the
overflow operations, which is work which will be submitted in a
following PR.
@codecov
Copy link

codecov bot commented Mar 11, 2022

Codecov Report

Merging #6722 (5ecedf8) into develop (ee16d80) will increase coverage by 0.04%.
The diff coverage is 79.34%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #6722      +/-   ##
===========================================
+ Coverage    76.80%   76.84%   +0.04%     
===========================================
  Files         1589     1589              
  Lines       183658   183798     +140     
===========================================
+ Hits        141056   141239     +183     
+ Misses       42602    42559      -43
Impacted Files Coverage Δ
src/solvers/flattening/bv_pointers.cpp 83.02% <0.00%> (-0.41%) ⬇️
src/util/pointer_expr.cpp 74.74% <0.00%> (+2.74%) ⬆️
src/util/pointer_expr.h 80.68% <0.00%> (+0.16%) ⬆️
src/analyses/goto_rw.cpp 62.35% <62.06%> (+6.45%) ⬆️
...c/solvers/smt2_incremental/convert_expr_to_smt.cpp 69.45% <97.14%> (+4.09%) ⬆️
src/analyses/dependence_graph.cpp 90.36% <100.00%> (+0.68%) ⬆️
src/analyses/dependence_graph.h 85.13% <100.00%> (+1.31%) ⬆️
src/analyses/goto_rw.h 68.42% <100.00%> (+3.03%) ⬆️
src/analyses/reaching_definitions.cpp 77.66% <100.00%> (+0.14%) ⬆️
...t/solvers/smt2_incremental/convert_expr_to_smt.cpp 100.00% <100.00%> (ø)
... and 9 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 29799b4...5ecedf8. Read the comment docs.

@thomasspriggs thomasspriggs merged commit 7127c4d into diffblue:develop Mar 11, 2022
@thomasspriggs thomasspriggs deleted the tas/more_smt_bitwise branch March 11, 2022 17:16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@NlightNFotis NlightNFotis NlightNFotis approved these changes

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

@TGWDB TGWDB Awaiting requested review from TGWDB TGWDB is a code owner

@chris-ryder chris-ryder Awaiting requested review from chris-ryder

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@thomasspriggs @NlightNFotis